(declare-fun |c_linear_search_#in~n| () Int)
(declare-fun |c_linear_search_#in~n_primed| () Int)
(declare-fun |c_linear_search_#t~short1| () Bool)
(declare-fun |c_linear_search_#t~short1_primed| () Bool)
(declare-fun c_linear_search_~n () Int)
(declare-fun c_linear_search_~n_primed () Int)
(declare-fun c_linear_search_~j~0 () Int)
(declare-fun c_linear_search_~j~0_primed () Int)
(push)
(assert (and (= c_linear_search_~j~0_primed (+ c_linear_search_~j~0 1)) (not (and (or (<= (+ (div c_linear_search_~n 4294967296) 1) 0) (<= c_linear_search_~n |c_linear_search_#in~n|)) (or (< 0 (+ (div c_linear_search_~n 4294967296) 1)) (<= |c_linear_search_#in~n| (+ (* 4294967296 (div c_linear_search_~n 4294967296)) 4294967295))) (<= c_linear_search_~j~0_primed 1) (< 0 (+ (div c_linear_search_~j~0_primed 4294967296) 1)))) (or (< 0 (+ (div c_linear_search_~n 4294967296) 1)) (<= |c_linear_search_#in~n| (+ (* 4294967296 (div c_linear_search_~n 4294967296)) 4294967295))) (or (<= (+ (div c_linear_search_~n 4294967296) 1) 0) (<= c_linear_search_~n |c_linear_search_#in~n|)) (= c_linear_search_~j~0 0) |c_linear_search_#t~short1|))
(check-sat)
(pop)
